(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 16))
(declare-fun v1 () (_ BitVec 12))
(declare-fun a2 () (Array  (_ BitVec 13)  (_ BitVec 14)))
(assert (let ((e3(_ bv58043 16)))
(let ((e4(_ bv4992 13)))
(let ((e5 (bvurem ((_ sign_extend 1) v1) e4)))
(let ((e6 (bvsub e3 ((_ sign_extend 3) e4))))
(let ((e7 (ite (bvsge v0 e3) (_ bv1 1) (_ bv0 1))))
(let ((e8 (store a2 ((_ extract 14 2) v0) ((_ sign_extend 2) v1))))
(let ((e9 (store e8 e4 ((_ extract 14 1) e6))))
(let ((e10 (store e8 e5 ((_ extract 15 2) e6))))
(let ((e11 (select a2 ((_ sign_extend 12) e7))))
(let ((e12 (select a2 ((_ sign_extend 12) e7))))
(let ((e13 (select e9 ((_ extract 15 3) v0))))
(let ((e14 (store e10 e5 ((_ sign_extend 13) e7))))
(let ((e15 (select e10 ((_ sign_extend 12) e7))))
(let ((e16 (store e10 e5 ((_ extract 15 2) e3))))
(let ((e17 (select e10 ((_ extract 14 2) e3))))
(let ((e18 (bvxnor e4 e5)))
(let ((e19 (ite (bvule e15 e12) (_ bv1 1) (_ bv0 1))))
(let ((e20 (ite (bvule v0 e3) (_ bv1 1) (_ bv0 1))))
(let ((e21 (bvand e17 e12)))
(let ((e22 (bvxor ((_ sign_extend 2) e15) v0)))
(let ((e23 (bvmul e6 ((_ sign_extend 2) e11))))
(let ((e24 (ite (bvugt ((_ sign_extend 4) v1) e6) (_ bv1 1) (_ bv0 1))))
(let ((e25 (bvnand v0 ((_ sign_extend 3) e4))))
(let ((e26 (bvneg e19)))
(let ((e27 (bvlshr e25 v0)))
(let ((e28 (bvashr e13 e17)))
(let ((e29 (bvcomp ((_ sign_extend 13) e7) e12)))
(let ((e30 (bvsge e6 ((_ zero_extend 2) e12))))
(let ((e31 (bvsge ((_ sign_extend 2) e11) e6)))
(let ((e32 (bvule e15 ((_ sign_extend 13) e26))))
(let ((e33 (= e13 e13)))
(let ((e34 (bvugt v0 ((_ sign_extend 2) e11))))
(let ((e35 (bvslt ((_ sign_extend 2) v1) e13)))
(let ((e36 (= e11 ((_ sign_extend 1) e5))))
(let ((e37 (bvslt e15 ((_ zero_extend 1) e18))))
(let ((e38 (bvule e11 ((_ sign_extend 13) e24))))
(let ((e39 (bvsgt e27 e23)))
(let ((e40 (bvuge e11 ((_ sign_extend 2) v1))))
(let ((e41 (bvsgt ((_ sign_extend 2) e11) e27)))
(let ((e42 (bvugt v1 ((_ zero_extend 11) e29))))
(let ((e43 (bvslt e17 ((_ zero_extend 13) e19))))
(let ((e44 (bvult ((_ zero_extend 1) e5) e11)))
(let ((e45 (= e27 ((_ sign_extend 15) e19))))
(let ((e46 (bvult v0 ((_ sign_extend 2) e11))))
(let ((e47 (bvslt e25 ((_ sign_extend 3) e18))))
(let ((e48 (bvsgt v1 v1)))
(let ((e49 (bvult e17 ((_ sign_extend 13) e7))))
(let ((e50 (bvsgt ((_ sign_extend 12) e7) e18)))
(let ((e51 (bvsle e15 ((_ zero_extend 13) e7))))
(let ((e52 (bvule ((_ sign_extend 13) e26) e13)))
(let ((e53 (bvult ((_ zero_extend 2) e17) e3)))
(let ((e54 (= ((_ sign_extend 4) v1) v0)))
(let ((e55 (bvsle e23 ((_ sign_extend 15) e29))))
(let ((e56 (bvule e17 e28)))
(let ((e57 (bvsle ((_ zero_extend 15) e19) e6)))
(let ((e58 (bvsge e22 ((_ sign_extend 3) e5))))
(let ((e59 (distinct ((_ sign_extend 2) e17) v0)))
(let ((e60 (bvult ((_ zero_extend 15) e7) e6)))
(let ((e61 (bvslt ((_ sign_extend 2) e13) e6)))
(let ((e62 (bvule ((_ zero_extend 12) e19) e4)))
(let ((e63 (bvsgt e17 e17)))
(let ((e64 (bvslt ((_ zero_extend 13) e20) e17)))
(let ((e65 (bvult ((_ sign_extend 13) e19) e17)))
(let ((e66 (bvule v0 ((_ sign_extend 2) e15))))
(let ((e67 (bvsle e22 ((_ zero_extend 2) e12))))
(let ((e68 (bvsgt e11 ((_ zero_extend 1) e18))))
(let ((e69 (bvsge ((_ zero_extend 13) e7) e13)))
(let ((e70 (bvsgt e3 ((_ sign_extend 15) e7))))
(let ((e71 (distinct ((_ sign_extend 15) e19) e23)))
(let ((e72 (bvult e23 ((_ zero_extend 2) e11))))
(let ((e73 (bvslt e11 e15)))
(let ((e74 (bvuge ((_ sign_extend 13) e24) e28)))
(let ((e75 (bvule ((_ sign_extend 1) e5) e21)))
(let ((e76 (xor e42 e74)))
(let ((e77 (and e65 e49)))
(let ((e78 (xor e35 e63)))
(let ((e79 (xor e60 e57)))
(let ((e80 (and e66 e48)))
(let ((e81 (or e44 e36)))
(let ((e82 (= e31 e51)))
(let ((e83 (xor e52 e71)))
(let ((e84 (ite e39 e62 e59)))
(let ((e85 (and e38 e64)))
(let ((e86 (ite e32 e76 e41)))
(let ((e87 (xor e73 e43)))
(let ((e88 (= e75 e79)))
(let ((e89 (and e83 e80)))
(let ((e90 (xor e78 e55)))
(let ((e91 (ite e50 e46 e53)))
(let ((e92 (and e77 e54)))
(let ((e93 (or e45 e47)))
(let ((e94 (not e85)))
(let ((e95 (= e67 e86)))
(let ((e96 (= e93 e81)))
(let ((e97 (or e30 e84)))
(let ((e98 (not e68)))
(let ((e99 (= e37 e34)))
(let ((e100 (or e88 e95)))
(let ((e101 (not e91)))
(let ((e102 (= e56 e97)))
(let ((e103 (and e99 e100)))
(let ((e104 (not e103)))
(let ((e105 (ite e58 e72 e69)))
(let ((e106 (and e105 e104)))
(let ((e107 (xor e70 e94)))
(let ((e108 (and e96 e92)))
(let ((e109 (ite e107 e61 e33)))
(let ((e110 (and e90 e40)))
(let ((e111 (= e98 e87)))
(let ((e112 (xor e106 e108)))
(let ((e113 (and e112 e112)))
(let ((e114 (and e110 e102)))
(let ((e115 (=> e82 e114)))
(let ((e116 (=> e109 e113)))
(let ((e117 (=> e116 e116)))
(let ((e118 (=> e111 e115)))
(let ((e119 (xor e118 e117)))
(let ((e120 (not e119)))
(let ((e121 (ite e89 e120 e120)))
(let ((e122 (and e121 e101)))
(let ((e123 (and e122 (not (= e4 (_ bv0 13))))))
e123
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
